

(define r1 (and (eq (to-i 1u) 1)
                (eq (to-i 1)  1)
                (eq (to-i 1i32) 1)
                (eq (to-i 1u32) 1)
                (eq (to-i 1i64) 1)
                (eq (to-i 1u64) 1)
                (eq (to-i 1.0f32) 1)
                (eq (to-i 1.0f64) 1)))

(define r2 (and (eq (to-u 1u) 1u)
                (eq (to-u 1)  1u)
                (eq (to-u 1i32) 1u)
                (eq (to-u 1u32) 1u)
                (eq (to-u 1i64) 1u)
                (eq (to-u 1u64) 1u)
                (eq (to-u 1.0f32) 1u)
                (eq (to-u 1.0f64) 1u)))

(define r3 (and (eq (to-i32 1u) 1i32)
                (eq (to-i32 1)  1i32)
                (eq (to-i32 1i32) 1i32)
                (eq (to-i32 1u32) 1i32)
                (eq (to-i32 1i64) 1i32)
                (eq (to-i32 1u64) 1i32)
                (eq (to-i32 1.0f32) 1i32)
                (eq (to-i32 1.0f64) 1i32)))

(define r4 (and (eq (to-u32 1u) 1u32)
                (eq (to-u32 1)  1u32)
                (eq (to-u32 1i32) 1u32)
                (eq (to-u32 1u32) 1u32)
                (eq (to-u32 1i64) 1u32)
                (eq (to-u32 1u64) 1u32)
                (eq (to-u32 1.0f32) 1u32)
                (eq (to-u32 1.0f64) 1u32)))

(check (and r1 r2 r3 r4)) 
